abstract-chain-replication{i:l}
abstract-chain-replication(es; Cmd; Rsp; isupdate; In; Out; Sys; f; Delta; Q)
== fifo-antecedent(es;Sys;f)
== & (u:E(Sys). (f(u) = u)  ((u  In)))
== & (E(In) r E(Sys))
== & (E(Out) r E(Sys))
== & (e:E(In). (((isupdate(In(e)))))  ((e  Out)))
== & (e:E(Sys). (((e  In)))  (loc(f(e)) = loc(e))  (((e  Out))))
== & input-forwarding{i:l}
== & input-forwarding(es; Cmd; Sys; isupdate; In; f)
== & (chain:E(Sys)(Id List). chain-consistent(f;chain))
== & (e:E(Out).
== & ((is-query(In;isupdate;e)
== & (( (Out(e) = Q(filter(isupdate;es-interface-history(es; Sys; e)),In(e))))
== & (& ((is-query(In;isupdate;e))
== & (& ( (Out(e) = Delta(filter(isupdate;es-interface-history(es; Sys; e)))))) 

latex

---

clarification:

abstract-chain-replication{i:l}
abstract-chain-replication(es; Cmd; Rsp; isupdate; In; Out; Sys; f; Delta; Q)
== fifo-antecedent(es;Sys;f)
== & (u:es-E-interface(es;Sys). (f(u) = u  es-E(es))  ((u  In)))
== & (es-E-interface(es;In) r es-E-interface(es;Sys))
== & (es-E-interface(es;Out) r es-E-interface(es;Sys))
== & (e:es-E-interface(es;In). (((isupdate(In(e)))))  ((e  Out)))
== & (e:es-E-interface(es;Sys).
== & ((((e  In)))  (es-loc(es; (f(e))) = es-loc(es; e)  Id)  (((e  Out))))
== & input-forwarding{i:l}
== & input-forwarding(es; Cmd; Sys; isupdate; In; f)
== & (chain:es-E-interface(es;Sys)(Id List). chain-consistent(es;Sys;In;isupdate;Out;f;chain))
== & (e:es-E-interface(es;Out).
== & ((is-query(In;isupdate;e)
== & (( (Out(e) = Q(filter(isupdate;es-interface-history(es; Sys; e)),In(e))  Rsp))
== & (& ((is-query(In;isupdate;e))
== & (& ( (Out(e) = Delta(filter(isupdate;es-interface-history(es; Sys; e)))  Rsp))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	abstract-chain-replication wf
Definitions	fifo-antecedent(es;Sys;f), P  Q, E, loc(e), b, e  X, input-forwarding{i:l}(es; Cmd; Sys; isupdate; In; f), x:A. B(x), x:AB(x), type List, Id, chain-consistent(f;chain), x:A. B(x), E(X), P & Q, P  Q, A, is-query(In;isupdate;e), s = t, X(e), f(a), filter(P;l), es-interface-history(es; X; e)
FDL editor aliases	abstract-chain-replication